minus(x, y) → cond(gt(x, y), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
minus(x, y) → cond(gt(x, y), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
MINUS(x, y) → COND(gt(x, y), x, y)
MINUS(x, y) → GT(x, y)
GT(s(u), s(v)) → GT(u, v)
COND(true, x, y) → MINUS(x, s(y))
minus(x, y) → cond(gt(x, y), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS(x, y) → COND(gt(x, y), x, y)
MINUS(x, y) → GT(x, y)
GT(s(u), s(v)) → GT(u, v)
COND(true, x, y) → MINUS(x, s(y))
minus(x, y) → cond(gt(x, y), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
GT(s(u), s(v)) → GT(u, v)
minus(x, y) → cond(gt(x, y), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GT(s(u), s(v)) → GT(u, v)
The value of delta used in the strict ordering is 85/16.
POL(s(x1)) = 5/4 + (15/4)x_1
POL(GT(x1, x2)) = x_1 + (13/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
minus(x, y) → cond(gt(x, y), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
MINUS(x, y) → COND(gt(x, y), x, y)
COND(true, x, y) → MINUS(x, s(y))
minus(x, y) → cond(gt(x, y), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)